\begin{tabbing}
$\forall$${\it the\_w}$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ (\=$\forall$$e$, ${\it e'}$:E.\+
\\[0ex]isrcv(kind($e$))
\\[0ex]$\Rightarrow$ isrcv(kind(${\it e'}$))
\\[0ex]$\Rightarrow$ lnk(kind($e$)) $=$ lnk(kind(${\it e'}$)) $\in$ IdLnk
\\[0ex]$\Rightarrow$ (\=$e$ $<$c ${\it e'}$\+
\\[0ex]$\Leftrightarrow$
\\[0ex]sender($e$) $<$c sender(${\it e'}$) $\vee$ sender($e$) $=$ sender(${\it e'}$) $\in$ E \& index($e$)$<$index(${\it e'}$)))
\-\-
\end{tabbing}